Multi-threading is a powerful technique for exploiting the inherent parallelism in contemporary computer systems. As a result, the use of concurrent multi-threaded programs is pervasive. Examples of multi-threaded programs include operating systems, databases and innumerable embedded systems e.g., cellular telephones, consumer electronics. Given their importance, the ability to analyze, debug and verify multi-threaded programs is of great interest.
As known by those skilled in the art common verification techniques do not scale adequately for the verification of large scale multi-threaded programs. As a result, techniques that permit their verification would represent a significant advance in the art.